Nuprl Definition : qrng 11,40

qrng
== <rationals
== , x,y. qeq(x; y)
== , x,y. q_le(x; y)
== , x,y. x + y
== , 0
== , x.-(x)
== , x,y. x * y
== , 1
== , x,y. if qeq(y; 0) then inr   else inl qdiv(x; y)  fi > 
latex



clarification:

qrng
== <rationals
== , x,y. qeq(x; y)
== , x,y. q_le(x; y)
== , x,y. x + y
== , 0
== , x.(-1) * x
== , x,y. x * y
== , 1
== , x,y. if qeq(y; 0) then inr   else inl qdiv(x; y)  fi > 
latex


Definitionsrationals, q_le(r; s), r + s, -n, r * s, <a, b>, x.A(x), if b then t else f fi , qeq(r; s), #$n, inr x , , inl x , qdiv(r; s)
FDL editor aliasesqrng

origin